(* Basic inversion lemmas ***************************************************)
-fact simple_inv_bind_aux: â\88\80T. ð\9d\95\8a[T] → ∀J,W,U. T = ⓑ{J} W. U → False.
+fact simple_inv_bind_aux: â\88\80T. ð\9d\90\92[T] → ∀J,W,U. T = ⓑ{J} W. U → False.
#T * -T
[ #I #J #W #U #H destruct
| #I #V #T #J #W #U #H destruct
]
qed.
-lemma simple_inv_bind: â\88\80I,V,T. ð\9d\95\8a[ⓑ{I} V. T] → False.
+lemma simple_inv_bind: â\88\80I,V,T. ð\9d\90\92[ⓑ{I} V. T] → False.
/2 width=6/ qed-.