Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Theorem disjoint__app_NoDup :
- forall (X : Type) (l1 l2 : list X) (default:X),
- disjoint X l1 l2 default ->
- NoDup X (l1 ++ l2) default.
- Proof.
- intros. induction H eqn:caseEqn.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement