proposition: Theorem appendSup : forall L1 L2 L3 : list A, append L1 L2 L3 -> forall a : A, (forall b : A, In b L1 -> ltA a b) -> (forall b : A, In b L2 -> ltA a b) -> forall b : A, In b L3 -> ltA a b.
proof: Proof. intros L1 L2 L3 H'; elim H'; simpl in |- *; auto; intros a b L4 L5 L6 H'0 H'1 H'2 a0 H'3 H'4 b0 H'5; (Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)