proposition: Lemma wf_map1': forall (A B: Type) (f: A -> B) (m: ptrie A) opt, wf opt m -> wf opt (map1' f m).
proof: Proof. induction m; intros. - simpl; constructor. - simpl. inv H; constructor; auto. - simpl. inv H; econstructor; trivial; try eassumption. + destruct m1; simpl; congruence. + destruct m2; simpl; congruence. + auto. + auto. + destruct m1; simpl; congruence. + destruct m2; simpl; congruence. + auto. + auto. Qed.
imports: Lia Cdcl.Coqlib