qed.
lemma trf_inv_atom: โI. โ[๐{I}] โ False.
-/2/ qed-.
+/2 width=4/ qed-.
fact trf_inv_abst_aux: โW,U,T. โ[T] โ T = ๐{Abst} W. U โ โ[W] โจ โ[U].
#W #U #T * -T
-[ #V #T #HV #H destruct -V T /2/
-| #V #T #HT #H destruct -V T /2/
+[ #V #T #HV #H destruct /2 width=1/
+| #V #T #HT #H destruct /2 width=1/
| #V #T #_ #H destruct
| #V #T #_ #H destruct
| #V #T #H destruct
qed.
lemma trf_inv_abst: โV,T. โ[๐{Abst}V.T] โ โ[V] โจ โ[T].
-/2/ qed-.
+/2 width=3/ qed-.
fact trf_inv_appl_aux: โW,U,T. โ[T] โ T = ๐{Appl} W. U โ
โจโจ โ[W] | โ[U] | (๐[U] โ False).
#W #U #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
-| #V #T #HV #H destruct -V T /2/
-| #V #T #HT #H destruct -V T /2/
+| #V #T #HV #H destruct /2 width=1/
+| #V #T #HT #H destruct /2 width=1/
| #V #T #H destruct
| #V #T #H destruct
-| #V #W0 #T #H destruct -V U
+| #V #W0 #T #H destruct
@or3_intro2 #H elim (simple_inv_bind โฆ H)
]
qed.
lemma trf_inv_appl: โW,U. โ[๐{Appl}W.U] โ โจโจ โ[W] | โ[U] | (๐[U] โ False).
-/2/ qed-.
+/2 width=3/ qed-.
lemma tif_inv_abbr: โV,T. ๐[๐{Abbr}V.T] โ False.
-/2/ qed-.
+/2 width=1/ qed-.
lemma tif_inv_abst: โV,T. ๐[๐{Abst}V.T] โ ๐[V] โง ๐[T].
-/4/ qed-.
+/4 width=1/ qed-.
lemma tif_inv_appl: โV,T. ๐[๐{Appl}V.T] โ โงโง ๐[V] & ๐[T] & ๐[T].
-#V #T #HVT @and3_intro /3/
-generalize in match HVT -HVT; elim T -T //
-* // * #U #T #_ #_ #H elim (H ?) -H /2/
+#V #T #HVT @and3_intro /3 width=1/
+generalize in match HVT; -HVT elim T -T //
+* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
qed-.
lemma tif_inv_cast: โV,T. ๐[๐{Cast}V.T] โ False.
-/2/ qed-.
+/2 width=1/ qed-.
(* Basic properties *********************************************************)
lemma tif_atom: โI. ๐[๐{I}].
-/2/ qed.
+/2 width=4/ qed.
lemma tif_abst: โV,T. ๐[V] โ ๐[T] โ ๐[๐ {Abst}V.T].
#V #T #HV #HT #H
-elim (trf_inv_abst โฆ H) -H /2/
+elim (trf_inv_abst โฆ H) -H /2 width=1/
qed.
lemma tif_appl: โV,T. ๐[V] โ ๐[T] โ ๐[T] โ ๐[๐{Appl}V.T].
#V #T #HV #HT #S #H
-elim (trf_inv_appl โฆ H) -H /2/
+elim (trf_inv_appl โฆ H) -H /2 width=1/
qed.