proposition: Lemma beta_notFunS: forall M N, M -b-> N -> isFunS M -> False.
proof: Proof. intros M N MN. term_inv M. unfold Tr in MN. inversion MN; term_inv M. inversion H; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)