proposition: Lemma interp_check_clause c1 : forall c2, forallb2 (fun i j => i =? j) c1 c2 -> C.interp rho c1 = C.interp rho c2.
proof: Proof. induction c1 as [ |l1 c1 IHc1]; simpl; intros [ |l2 c2]; simpl; auto; try discriminate. unfold is_true. rewrite andb_true_iff. intros [H1 H2]. rewrite Int63.eqb_spec in H1. now rewrite (IHc1 _ H2), H1. Qed.
imports: State SMT_terms List Bool PArray Int63