proposition: Lemma type_var : forall e x tau, In (Id x) (vars_with_type e tau) <-> typing e (Id x) tau.
proof: Proof. induction e as [| tau e IHe]; move => x tau' /=. - split; intros H; solve [exfalso; auto | inversion H; subst; destruct x; simpl in *; discriminate ]. - split; rewrite /vars_with_type /=; intros H; destruct (type_eq_dec tau' tau); subst. + destruct x; simpl in *; auto. constructor; auto. inversion H as [H1 | H1]; try discriminate. setoid_rewrite vars_with_type_shift in H1. apply IHe in H1. inversion H1; subst. constructor; auto. + destruct x; simpl in *; auto. constructor; auto. apply vars_with_type_le in H. lia. setoid_rewrite vars_with_type_shift in H. apply IHe in H. inversion H; subst. constructor; auto. + destruct x; simpl in *; auto. right. rewrite vars_with_type_shift. apply IHe. inversion H. simpl in *. constructor; auto. + destruct x; simpl in *; auto. inversion H; subst. simpl in *. exfalso; auto. inversion H1; auto. rewrite vars_with_type_shift. apply IHe. inversion H; subst. constructor; auto. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) String QuickChick(QuickChick) Arith List Lia QuickChick.stlc(lambda) Wellfounded