proposition: Lemma ex_eql : forall l1 l2, (exists A , exists B, Len A B l1 /\ Len A B l2) -> l1 =l= l2.
proof: Proof. intros. ex_and H A. ex_and H0 B. assert(HH:=H). assert(HH0:=H0). unfold Len in HH. unfold Len in HH0. spliter. unfold EqL. repeat split; auto. intro. assert(Len A0 B0 l1). unfold Len. split; auto. assert(Cong A B A0 B0). apply (is_len_cong _ _ _ _ l1); auto. assert(Len A0 B0 l2). apply(is_len_cong_is_len A B). apply H0. auto. unfold Len in H8. spliter. auto. intro. assert(Len A0 B0 l2). unfold Len. split; auto. assert(Cong A B A0 B0). apply (is_len_cong _ _ _ _ l2); auto. assert(Len A0 B0 l1). apply(is_len_cong_is_len A B). apply H. auto. unfold Len in H8. spliter. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 Setoid