DEFINITION pr3_iso_beta()
TYPE =
       ∀v:T
         .∀w:T
           .∀t:T
             .let u1 := 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 (THead (Bind Abbr) v t) u2)
BODY =
Show proof