Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Theorem test2: forall (a: nat) (c: Type), maybe_return _ a a c = Some c.
- Proof.
- intros.
- simpl.
- unfold maybe_return.
- compute.
- Admitted.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
