proposition: Lemma lg_null_instance : forall l A, Q_Cong_Null l -> l A A.
proof: Proof. intros. unfold Q_Cong_Null in H. spliter. unfold Q_Cong in H. ex_and H X. ex_and H1 Y. assert(HH:= H A A). destruct HH. ex_and H0 P. assert(HH:=(H P P)). destruct HH. apply H4 in H3. apply H1. apply cong_symmetry in H3. apply cong_reverse_identity in H3. subst Y. apply cong_trivial_identity. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1