proposition: Lemma fin_branch_supterm : finitely_branching supterm.
proof: Proof. intros x. exists (subterm_lst x). pattern x; apply term_ind_forall; clear x. simpl. intros v y. split; try tauto. intro HS; destruct HS as [c Hc]. destruct (var_eq_fill (proj2 Hc)) as [Hc' _]; intuition. intros f ts Hts y. split; rewrite subterm_lst_fun, in_app. 2:{ intuition. gen (in_list_of_vec H0). apply subterm_fun. ded (In_subterm_lst_vec_elim _ _ H0). decomp H. ded (Vforall_nth x0 Hts y). apply (@subterm_trans _ _ (Vnth ts x0)). apply H. hyp. apply subterm_fun. apply Vnth_in. } intros. destruct H as [c Hc]. destruct (fun_eq_fill (proj2 Hc)). intuition. destruct H as [i H]. destruct H as [j H]. destruct H as [r H]. destruct H as [ti H]. destruct H as [c0 H]. destruct H as [tj Hc0]. destruct Hc as [Hc Hf]. rewrite Hc0 in Hf. simpl in Hf. Funeqtac. destruct c0. simpl in H. left. rewrite H. apply list_of_vec_in. apply Vin_cast_intro. apply Vin_appr. simpl. left; refl. right. assert (p : i < arity f). rewrite <- r. lia. assert (Hs : supterm (Vnth ts p) y). rewrite H, Vnth_cast, Vnth_app. destruct (le_gt_dec i i). 2: lia. set (q := (Vnth_app_aux (S j) (Vnth_cast_aux r p) l)). rewrite (Vnth_eq _ q (Nat.lt_0_succ j)); try lia. simpl. exists (Cont f0 e t c0 t0). simpl. intuition. discr. ded (Vforall_nth p Hts y). apply (In_subterm_lst_vec_intro _ _ p). apply (proj1 H0). auto. Qed.
imports: CoLoR(AContext VecUtil ListUtil LogicUtil NatUtil RelUtil ASN)