-[ #V #T #F1 #H
- elim (booleanized_inv_appl … H) -H #c #W #U #H destruct
-| #b #p #T1 #T2 #_ #IHT12 #F1 #H
- elim (booleanized_inv_abst … H) -H /2 width=2/
-| #b #p #V1 #V2 #T #_ #IHV12 #F1 #H
- elim (booleanized_inv_appl … H) -H /2 width=2/
-| #b #p #V #T1 #T2 #_ #IHT12 #F1 #H
- elim (booleanized_inv_appl … H) -H /2 width=2/
+[ #V #T #M1 #H
+ elim (boolean_inv_appl … H) -H #B #A #H destruct
+| #b #p #T1 #T2 #_ #IHT12 #M1 #H
+ elim (boolean_inv_abst … H) -H /2 width=2/
+| #b #p #V1 #V2 #T #_ #IHV12 #M1 #H
+ elim (boolean_inv_appl … H) -H /2 width=2/
+| #b #p #V #T1 #T2 #_ #IHT12 #M1 #H
+ elim (boolean_inv_appl … H) -H /2 width=2/