proposition: Lemma typing_max_no_app : forall e t tau, app_free t -> typing e t tau -> typing_max_tau e t tau 0.
proof: Proof. intros e t tau H. generalize e tau. clear e tau. induction H; intros e tau H1; inversion H1; subst; constructor; auto. Qed.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)