proposition: Lemma typing_max_tau_correct : forall e t tau, (exists m, typing_max_tau e t tau m) <-> typing e t tau.
proof: Proof. intros. split. - move => [maxt H]. induction H; econstructor; eauto. - move => H. induction H; (try now eexists; econstructor; eauto). destruct IHtyping as [m H']. exists m. constructor; auto. destruct IHtyping1 as [m1 H1]; destruct IHtyping2 as [m2 H2]. eexists. econstructor; eauto. Qed.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)