proposition: Lemma Equal_Tlist_equiv : Equivalence Equal_Tlist.
proof: Proof. apply Build_Equivalence. unfold Reflexive in |- *; intro l; elim l; simpl in |- *. auto. intros; split; [ apply Refl | auto ]. apply Build_Partial_equivalence. unfold Transitive in |- *; intros l1; elim l1. intro l2; elim l2. intro l3; elim l3; simpl in |- *; trivial. intros c t H z H1; elim H1. intros c t H y; elim y. intros z H1 H2; elim H1. intros c0 t0 H0 z; elim z. intros H1 H2; elim H2. intros c1 t1 H1 H2 H3. elim H2; intros H4 H5. elim H3; intros H6 H7. simpl in |- *; split. apply Trans with c0; trivial. apply (H t0 t1); trivial. unfold Symmetric in |- *; intro l1; elim l1. intro l2; elim l2. trivial. intros c t H H1; elim H1. intros c t H l2; elim l2. simpl in |- *; trivial. intros c0 t0 H0 H1. elim H1; intros H2 H3. simpl in |- *; split. apply Sym; trivial. apply H; trivial. Qed.
imports: Monoid