proposition: Lemma disjoint_cons_l_inv : forall x v l1 l2, disjoint ((x,v)::l1) l2 -> disjoint l1 l2.
proof: Proof. Proof using. introv M. intros y v1 v2 K1 K2. tests C: (x = y). { applys M v v2 K2. rewrite get_opt_cons. case_if~. } { applys M v1 v2 K2. rewrite get_opt_cons. case_if~. } Qed.
imports: TLC(LibTactics LibReflect)