proposition: Lemma not_over_not_lin_nvar : forall (v : NVar) l t, !(LIn v l # t) <=> (!LIn v l [+] !t).
proof: Proof. introv; split; intro k; repnd; sp. generalize (in_deq NVar deq_nvar v l); intro o; sp. right; intro j. apply k; sp. Qed.
imports: list Omega