Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Inductive A :=
- mkA : nat -> A.
- Lemma constructor_functional :
- forall i1 i2, mkA i1 <> mkA i2 -> i1 <> i2.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement