proposition: Theorem OlistIn : forall (L : list A) (a b : A), In a L -> In b L -> Olist L -> eqA a b -> a = b.
proof: Proof. intros L; elim L; simpl in |- *; auto. intros a b H'; elim H'; auto. intros a l H' a0 b H'0; Elimc H'0; intros H'0; [ rewrite <- H'0 | idtac ]. intros H'1; Casec H'1; intros H'1; auto. intros H'2 H'3; absurd (eqA a b); auto. apply ltAImpNotEqA; auto. apply OlistSup with (L := l); auto. intros H'1; Elimc H'1; intros H'1; [ rewrite <- H'1 | idtac ]; intros H'2 H'3. absurd (eqA a a0); auto. apply ltAImpNotEqA; auto. apply OlistSup with (L := l); auto. apply H'; auto. apply OlistInv with (a := a); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)