proposition: Lemma typesUpTo_correct: forall n t, type_depth t <= n <-> List.In t (typesUpTo n).
proof: Proof. induction n; intros; split; intros. - destruct t; simpl in *; lia. - simpl in *. contradiction. - simpl. destruct t; [auto|]. right. simpl in *. match goal with | |- In ?e (map ?f _) => change e with (f (t1, t2)) end. apply in_map. apply in_prod; eapply IHn; lia. - simpl in *. destruct H. + subst. simpl. lia. + apply in_map_iff in H. destruct H as [[t1 t2] [? H]]. subst t. apply in_prod_iff in H. destruct H as [H1 H2]. pose proof ((proj2 (IHn _)) H1). pose proof ((proj2 (IHn _)) H2). simpl. lia. Qed.
imports: Arith Lia List