INDUCTIVE DEFINITION pr2 () [ ]
OF ARITY C→T→T→Prop
BUILT FROM:
     pr2_free: ∀c:C.∀t1:T.∀t2:T.(pr0 t1 t2)→(pr2 c t1 t2)
   | pr2_delta: ∀c:C
                         .∀d:C
                           .∀u:T
                             .∀i:nat
                               .getl i c (CHead d (Bind Abbr) u)
                                 →∀t1:T.∀t2:T.(pr0 t1 t2)→∀t:T.(subst0 i u t2 t)→(pr2 c t1 t)