proposition: Lemma lg_exists : forall A B, exists l, Q_Cong l /\ l A B.
proof: Proof. intros. unfold Q_Cong. exists (fun x y => Cong A B x y). split. exists A. exists B. intros. split; auto. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1