proposition: Lemma beta_var_normal : forall M N, isVar M -> ~(M -b-> N).
proof: Proof. intros M N Mvar MN. inversion MN; inversion H; term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)