proposition: Lemma valid_check_congr_pred : forall lpa lpb eqs, C.interp rho (check_congr_pred lpa lpb eqs).
proof: Proof. unfold check_congr_pred;intros. case_eq (t_form.[Lit.blit lpa]);auto with smtcoq_euf smtcoq_core. case_eq (t_form.[Lit.blit lpb]);auto with smtcoq_euf smtcoq_core;intros. case_eq (t_atom.[i0]);auto with smtcoq_euf smtcoq_core; case_eq (t_atom.[i]);auto with smtcoq_euf smtcoq_core;intros. destruct (Atom.reflect_uop_eqb u0 u);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). destruct (rho (Lit.blit lpa));reflexivity. rewrite !wf_interp_form, H, H0;simpl. generalize wt_t_atom;unfold Atom.wt;unfold is_true; rewrite Misc.aforallbi_spec;intros. assert (i <? length t_atom). apply PArray.get_not_default_lt. rewrite H1, def_t_atom;discriminate. assert (i0 <? length t_atom). apply PArray.get_not_default_lt. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. apply f_equal;apply f_equal. inversion H3;clear H3;subst;trivial with smtcoq_euf smtcoq_core. destruct (Atom.reflect_bop_eqb b0 b);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). destruct (rho (Lit.blit lpa));reflexivity. rewrite !wf_interp_form, H, H0;simpl. generalize wt_t_atom;unfold Atom.wt;unfold is_true; rewrite Misc.aforallbi_spec;intros. assert (i <? length t_atom). apply PArray.get_not_default_lt. rewrite H1, def_t_atom. discriminate. assert (i0 <? length t_atom). apply PArray.get_not_default_lt. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. inversion H3;clear H3;subst. inversion H11;clear H11;subst. apply f_equal; apply f_equal2;trivial with smtcoq_euf smtcoq_core. destruct (Misc.reflect_eqb i2 i1);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). destruct (rho (Lit.blit lpa));reflexivity. rewrite !wf_interp_form, H, H0;simpl. generalize wt_t_atom;unfold Atom.wt;unfold is_true; rewrite Misc.aforallbi_spec;intros. assert (i <? length t_atom). apply PArray.get_not_default_lt. rewrite H1, def_t_atom;discriminate. assert (i0 <? length t_atom). apply PArray.get_not_default_lt. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. apply f_equal;destruct (t_func.[i1]);apply f_equal. clear H H0 H1 H2 H5 H6. induction H3;simpl;trivial with smtcoq_euf smtcoq_core. unfold Atom.interp_hatom in H;rewrite H, IHForall2;trivial with smtcoq_euf smtcoq_core. Qed.
imports: Bool List Int63 PArray State SMT_terms