proposition: Lemma termsUpTo_correct: forall n t, term_depth t <= n <-> List.In t (termsUpTo n).
proof: Proof. induction n; intros; split; intros. - destruct t; simpl in *; lia. - simpl in *. contradiction. - destruct t; simpl in *. + do 0 (apply in_or_app; right). apply in_or_app; left. apply in_map. apply natsUpTo_correct. lia. + do 1 (apply in_or_app; right). apply in_or_app; left. match goal with | |- In ?e (map ?f _) => change e with (f (A, B, t)) end. repeat first [ apply in_map | apply in_prod | apply (proj1 (natsUpTo_correct _ _)) | apply (proj1 (typesUpTo_correct _ _)) | apply (proj1 (IHn _)) | lia]. + do 2 (apply in_or_app; right). apply in_or_app; left. match goal with | |- In ?e (map ?f _) => change e with (f (t1, t2)) end. repeat first [ apply in_map | apply in_prod | apply (proj1 (natsUpTo_correct _ _)) | apply (proj1 (typesUpTo_correct _ _)) | apply (proj1 (IHn _)) | lia]. + do 3 (apply in_or_app; right). simpl. auto. + do 3 (apply in_or_app; right). simpl. auto. + do 3 (apply in_or_app; right). simpl. right. right. repeat first [ apply in_map | apply in_prod | apply (proj1 (natsUpTo_correct _ _)) | apply (proj1 (typesUpTo_correct _ _)) | apply (proj1 (IHn _)) | lia]. - simpl in *. repeat ((simpl in H || apply in_app_iff in H || idtac); destruct H). + apply in_map_iff in H. destruct H as [x [? H]]. subst t. pose proof ((proj2 (natsUpTo_correct _ _)) H). simpl. lia. + apply in_map_iff in H. destruct H as [[[A B] body] [? H]]. subst t. repeat (apply in_prod_iff in H; destruct H). pose proof ((proj2 (typesUpTo_correct _ _)) H). pose proof ((proj2 (typesUpTo_correct _ _)) H1). pose proof ((proj2 (IHn _)) H0). simpl. lia. + apply in_map_iff in H. destruct H as [[t1 t2] [? H]]. subst t. repeat (apply in_prod_iff in H; destruct H). pose proof ((proj2 (IHn _)) H). pose proof ((proj2 (IHn _)) H0). simpl. lia. + simpl. lia. + simpl. lia. + apply in_map_iff in H. destruct H as [R [? H]]. subst t. pose proof ((proj2 (typesUpTo_correct _ _)) H). simpl. lia. Qed.
imports: Arith Lia List