proposition: Lemma var_comp : forall M, isVar M -> Computable M.
proof: Proof. intros M Mvar. assert (Mneutral: isNeutral M). term_inv M. apply (proj2 (neutral_comp_step (algebraic_var M Mvar) Mneutral)). intros N MN. absurd (M -R-> N); trivial. apply R_var_normal; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)