fact: Fixpoint bterm_rect (t : bterm) : P t := match t as t return P t with | BVar h => H1 h | BFun f v => let fix bterms_rect n (v : bterms n) : Q v := match v as v return Q v with | Vnil => H3 | Vcons t' v' => H4 (bterm_rect t') (bterms_rect _ v') end in H2 f (bterms_rect (arity f) v) end.
imports: CoLoR(ATerm VecUtil AInterpretation LogicUtil NatUtil)