proposition: Lemma vars_with_type_le_length: forall e x tau, In (Id x) (vars_with_type e tau) -> x < (length e).
proof: Proof. intros. apply vars_with_type_le_length_aux in H. unfold addn, addn_rec in *. lia. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) String QuickChick(QuickChick) Arith List Lia QuickChick.stlc(lambda) Wellfounded