proposition: Lemma size_subterm_at_pos : forall t i p, match subterm_at_pos t (i :: p) with | Some u => size u < size t | None => True end.
proof: Proof. intros t i p; generalize t i; clear t i; induction p as [ | j p]. intros [ v | f l ] j; simpl subterm_at_pos; cbv iota beta; trivial. generalize (nth_error_ok_in j l); destruct (nth_error l j) as [tj | ]; [idtac | trivial]. intro H; apply size_direct_subterm; simpl; apply H; trivial. intros [ v | f l ] i; simpl subterm_at_pos; cbv iota beta; trivial. generalize (nth_error_ok_in i l); destruct (nth_error l i) as [ti | ]; [idtac | trivial]. intro ti_in_l; generalize (IHp ti j); simpl subterm_at_pos; destruct ti as [vi | fi li]; trivial. generalize (nth_error_ok_in j li); destruct (nth_error li j) as [tij | ]; [idtac | trivial]. intro tij_in_li; destruct (subterm_at_pos tij p) as [ u | ]; trivial. intro H; apply lt_trans with (size (Term fi li)); trivial. apply size_direct_subterm; simpl; apply ti_in_l; trivial. Qed.
imports: List more_list list_permut list_set Arith