proposition: Lemma SortA_equivlistA_eqlistA : forall l l', SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
proof: Proof. intros l; induction l as [|a l IHl]; intros l'; destruct l' as [|a0 l']; simpl; intros H H0 H1; auto. - destruct (H1 a0); assert (InA a0 nil) by auto; inv. - destruct (H1 a); assert (InA a nil) by auto; inv. - inv. assert (forall y, InA y l -> ltA a y) by (intros; eapply (SortA_InfA_InA (l:=l)); eauto). assert (forall y, InA y l' -> ltA a0 y) by (intros; eapply (SortA_InfA_InA (l:=l')); eauto). do 2 match goal with H : InfA _ _ |- _ => clear H end. assert (eqA a a0). + destruct (H1 a). destruct (H1 a0). assert (InA a (a0::l')) by auto. inv; auto. assert (InA a0 (a::l)) by auto. inv; auto. elim (StrictOrder_Irreflexive a); eauto. + constructor; auto. apply IHl; auto. intros x; split; intros. * destruct (H1 x). assert (InA x (a0::l')) by auto. inv; auto. match goal with H3 : eqA a a0, H4 : InA x l, H9 : eqA x a0 |- InA x l' => rewrite H9,<-H3 in H4 end. elim (StrictOrder_Irreflexive a); eauto. * destruct (H1 x). assert (InA x (a::l)) by auto. inv; auto. match goal with H3 : eqA a a0, H4 : InA x l', H9 : eqA x a |- InA x l => rewrite H9,H3 in H4 end. elim (StrictOrder_Irreflexive a0); eauto. Qed.
imports: List Sorted Setoid Basics Morphisms