proposition: Lemma tilde_0_inj_neg : forall k k', (k~0)%positive <> (k'~0)%positive -> k <> k'.
proof: Proof. induction k; destruct k'; intuition; try match goal with | H : _ = _ |- _ => inversion H; clear H; subst end; intuition eauto. Qed.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases