-lemma swap_inj : \forall u,v,x,y.(swap u v x) = (swap u v y) \to x = y.
-intros;unfold swap in H;elim (eq_eqb_case x u)
- [elim H1;elim (eq_eqb_case y u)
- [elim H4;rewrite > H5;assumption
- |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
- elim (eq_eqb_case y v)
- [elim H7;rewrite > H9 in H;simplify in H;rewrite > H in H8;
- lapply (H5 H8);elim Hletin
- |elim H7;rewrite > H9 in H;simplify in H;elim H8;symmetry;assumption]]
- |elim H1;elim (eq_eqb_case y u)
- [elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
- elim (eq_eqb_case x v)
- [elim H7;rewrite > H9 in H;simplify in H;rewrite < H in H8;
- elim H2;assumption
- |elim H7;rewrite > H9 in H;simplify in H;elim H8;assumption]
- |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
- elim (eq_eqb_case x v)
- [elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
- [elim H10;rewrite > H11;assumption
- |elim H10;rewrite > H12 in H;simplify in H;elim H5;symmetry;
- assumption]
- |elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
- [elim H10;rewrite > H12 in H;simplify in H;elim H2;assumption
- |elim H10;rewrite > H12 in H;simplify in H;assumption]]]]
+theorem append_to_or_in_list: \forall A:Type.\forall x:A.
+\forall l,l1. x \in l@l1 \to (x \in l) \lor (x \in l1).
+intros 3.
+elim l
+ [right.apply H
+ |simplify in H1.inversion H1;intros; destruct;
+ [left.apply in_Base
+ | elim (H l2)
+ [left.apply in_Skip. assumption
+ |right.assumption
+ |assumption
+ ]
+ ]
+ ]