proposition: Lemma lg_eql_lg : forall l1 l2, Q_Cong l1 -> EqL l1 l2 -> Q_Cong l2.
proof: Proof. intros. unfold EqL in *. unfold Q_Cong in *. decompose [ex] H. exists x. exists x0. intros. rewrite H2. apply H0. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 Setoid