Advertisement
Guest User

Untitled

a guest
Jul 21st, 2017
43
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.11 KB | None | 0 0
  1. Inductive A :=
  2. mkA : nat -> A.
  3.  
  4. Lemma constructor_functional :
  5. forall i1 i2, mkA i1 <> mkA i2 -> i1 <> i2.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement