proposition: Lemma fix_reducts_vec : forall f ts k us h, (fix reducts_vec (k : nat) (us : terms k) : k <= arity f -> list term := match us in (vector _ k0) return (k0 <= arity f -> list term) with | Vnil => fun _ => nil | Vcons u1 us' => fun h => map (fun x => Fun f (Vreplace ts (reducts_aux2 h) x)) (reducts u1) ++ reducts_vec _ us' (reducts_aux1 h) end) k us h = reducts_vec f ts us h.
proof: Proof. induction us; simpl; intros. refl. apply app_eq. refl. apply IHus. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)