proposition: Lemma check_symopp_eq': forall ibs1 ibs2 xbs1 ybs2 ibsres zbsres n, check_symopp (ibs1 :: xbs1) (ibs2 :: ybs2) (ibsres :: zbsres) (BO_eq (Typ.TBV n)) = true -> Bool.eqb (Lit.interp rho ibs1) (Lit.interp rho ibs2) = Lit.interp rho ibsres.
proof: Proof. intros. simpl in H. case_eq (Lit.is_pos ibsres). intros. rewrite H0 in H. case_eq (t_form .[ Lit.blit ibsres]); intros; rewrite H1 in H; try (now contradict H). specialize (@rho_interp ( Lit.blit ibsres)). rewrite H1 in rho_interp. simpl in rho_interp. case_eq ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)). intros. rewrite orb_true_iff in H2. destruct H2. rewrite andb_true_iff in H2. destruct H2. rewrite eqb_spec in H2, H3. rewrite H2, H3 in rho_interp. rewrite <- rho_interp. unfold Lit.interp. rewrite H0. now unfold Var.interp. intros. rewrite andb_true_iff in H2. destruct H2. rewrite eqb_spec in H2, H3. rewrite H2, H3 in rho_interp. rewrite bool_eqb_comm in rho_interp. rewrite <- rho_interp. unfold Lit.interp. rewrite H0. now unfold Var.interp. intros. rewrite H2 in H. now contradict H. intros. rewrite H0 in H. now contradict H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance