proposition: Lemma map_lst: forall l i, match map (Lit.interp rho) l with | [] => [] | _ :: _ => Lit.interp rho i :: removelast (map (Lit.interp rho) l) end = map (Lit.interp rho) match l with | [] => [] | _ :: _ => i :: removelast l end.
proof: Proof. intro l. induction l; intros. now simpl. simpl. apply f_equal. now rewrite IHl. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance