INDUCTIVE DEFINITION
pr0 ()
[
]
OF ARITY
T→T→Prop
BUILT FROM:
pr0_refl: ∀t:T.(pr0 t t)
| pr0_comp: ∀u1:T.∀u2:T.(pr0 u1 u2)→∀t1:T.∀t2:T.(pr0 t1 t2)→∀k:K.(pr0 (THead k u1 t1) (THead k u2 t2))
| pr0_beta: ∀u:T
.∀v1:T
.∀v2:T
.pr0 v1 v2
→∀t1:T
.∀t2:T
.pr0 t1 t2
→(pr0
THead (Flat Appl) v1 (THead (Bind Abst) u t1)
THead (Bind Abbr) v2 t2)
| pr0_upsilon: ∀b:B
.not (eq B b Abst)
→∀v1:T
.∀v2:T
.pr0 v1 v2
→∀u1:T
.∀u2:T
.pr0 u1 u2
→∀t1:T
.∀t2:T
.pr0 t1 t2
→(pr0
THead (Flat Appl) v1 (THead (Bind b) u1 t1)
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2))
| pr0_delta: ∀u1:T
.∀u2:T
.pr0 u1 u2
→∀t1:T
.∀t2:T
.pr0 t1 t2
→∀w:T.(subst0 O u2 t2 w)→(pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 w))
| pr0_zeta: ∀b:B
.not (eq B b Abst)
→∀t1:T.∀t2:T.(pr0 t1 t2)→∀u:T.(pr0 (THead (Bind b) u (lift (S O) O t1)) t2)
| pr0_tau: ∀t1:T.∀t2:T.(pr0 t1 t2)→∀u:T.(pr0 (THead (Flat Cast) u t1) t2)