proposition: Lemma prop_eq_carry_lit2: forall a b, forallb2 eq_carry_lit a b = true -> (map interp_carry a) = (map (Lit.interp rho) b).
proof: Proof. intro a. induction a. - intros. simpl in H. case b in *. now simpl. now contradict H. - intros. case b in *. now simpl. simpl in *. rewrite andb_true_iff in H; destruct H. apply prop_eq_carry_lit in H. rewrite H. apply f_equal. now apply IHa. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance