proposition: Lemma disjoint_rem : forall a l1 l2, disjoint l1 l2 -> disjoint (rem a l1) (rem a l2).
proof: Proof. Proof using. introv D. intros y v1 v2 K1 K2. rewrite get_opt_rem in *. case_if~. applys* D K1 K2. Qed.
imports: TLC(LibTactics LibReflect)