proposition: Lemma vars_with_type_le_length_aux: forall e x tau n, In (Id x) (map (fun p : type * var => Id (snd p)) (filter (fun p : type * nat => proj1_sig (Sumbool.bool_of_sumbool (type_eq_dec tau (fst p)))) (combine e (seq n (length e))))) -> x < n + (length e).
proof: Proof. move => e. induction e; intros x tau n H; simpl in *. now exfalso; auto. unfold addn, addn_rec in *. destruct (type_eq_dec tau a); subst; simpl in *. destruct H. inversion H; subst. lia. apply IHe in H. lia. eapply IHe in H; lia. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) String QuickChick(QuickChick) Arith List Lia QuickChick.stlc(lambda) Wellfounded