proposition: Lemma stacc_intro' f (ts : TypArgs f) i (hi : Acc f i) t u : t = apps (Fun f) ts -> u = Vnth ts (Acc_arity hi) -> supterm_acc t u.
proof: Proof. intros e1 e2. subst. apply stacc_intro. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)