DEFINITION pr3_iso_appls_beta()
TYPE =
∀us:TList
.∀v:T
.∀w:T
.∀t:T
.let u1 := THeads
Flat Appl
us
THead (Flat Appl) v (THead (Bind Abst) w t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t)) u2)
BODY =
Show proof