proposition: Lemma vars_with_type_shift: forall e x tau n, In (Id (S 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 (S n) (length e))))) <-> 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))))).
proof: Proof. move => e. induction e; intros x tau; simpl in *; split; auto; intros H; destruct (type_eq_dec tau a); subst; simpl in *; try (destruct H; try (inversion H; auto)); try right; apply IHe; auto. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) String QuickChick(QuickChick) Arith List Lia QuickChick.stlc(lambda) Wellfounded