DEFINITION iso_flats_lref_bind_false()
TYPE =
       ∀f:F
         .∀b:B
           .∀i:nat
             .∀v:T
               .∀t:T
                 .∀vs:TList
                   .iso (THeads (Flat f) vs (TLRef i)) (THead (Bind b) v t)
                     →∀P:Prop.P
BODY =
Show proof