proposition: Lemma pmap_lookup_insert_None_neq : forall (m : pmap) (k : positive) (v : T) (k' : positive), k <> k' -> pmap_lookup k' m = None <-> pmap_lookup k' (pmap_insert k v m) = None.
proof: Proof. intros m k; revert m. induction k; simpl; intros; forward; Cases.rewrite_all_goal; autorewrite with pmap_rw; eauto. { destruct k'; simpl; destruct m; simpl; autorewrite with pmap_rw; Cases.rewrite_all_goal; try reflexivity. erewrite IHk; eauto using tilde_1_inj_neg. reflexivity. } { destruct k'; simpl; destruct m; simpl; autorewrite with pmap_rw; Cases.rewrite_all_goal; try reflexivity; try congruence. erewrite IHk. reflexivity. eauto using tilde_0_inj_neg. } { destruct k'; simpl; destruct m; simpl; autorewrite with pmap_rw; Cases.rewrite_all_goal; try reflexivity; try congruence. } Qed.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases