proposition: Lemma test_cong_ok : forall ss interp p1 p2 p3 p4, ss_ok ss interp -> test_cong ss p1 p2 p3 p4 = true -> CTCong (interp p1) (interp p2) (interp p3) (interp p4).
proof: Proof. intros ss interp p1 p2 p3 p4 HSS HTC. unfold test_cong in HTC. assert (HSS2 : ss_ok (identify_lengths ss) interp) by (apply identify_lengths_ok; assumption). unfold ss_ok in HSS2. apply SSPWEqP.MP.Dec.F.exists_2 in HTC. unfold SSP.Exists in HTC. destruct HTC as [s [HIn Hmem]]. apply HSS2 with s. apply SSPWEqP.MP.Dec.F.mem_1. assumption. assumption. intros x y Hxy. assert (HmemEq : forall p q, SP.mem (p,q) x = SP.mem (p,q) y) by (intros; apply SPWP.Dec.F.mem_m; [unfold Pos.eq|]; auto). rewrite 2 HmemEq; reflexivity. Qed.
imports: Recdef NArith GeoCoq.Utils.sets