proposition: Lemma vars_with_type_Id : forall e tau t, In t (vars_with_type e tau) -> exists x, t = Id x.
proof: Proof. intros. rewrite /vars_with_type /= in H. apply in_map_iff in H. destruct H as [[tau' x] [H1 H2]]. eexists; eauto. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) String QuickChick(QuickChick) Arith List Lia QuickChick.stlc(lambda) Wellfounded