DEFINITION iso_flats_flat_bind_false()
TYPE =
       ∀f1:F
         .∀f2:F
           .∀b:B
             .∀v:T
               .∀v2:T
                 .∀t:T
                   .∀t2:T
                     .∀vs:TList
                       .(iso
                           THeads (Flat f1) vs (THead (Flat f2) v2 t2)
                           THead (Bind b) v t)
                         →∀P:Prop.P
BODY =
Show proof