(* reducible terms *)
inductive trf: predicate term โ
-| trf_abst_sn: โV,T. trf V โ trf (๐{Abst} V. T)
-| trf_abst_dx: โV,T. trf T โ trf (๐{Abst} V. T)
-| trf_appl_sn: โV,T. trf V โ trf (๐{Appl} V. T)
-| trf_appl_dx: โV,T. trf T โ trf (๐{Appl} V. T)
-| trf_abbr : โV,T. trf (๐{Abbr} V. T)
-| trf_cast : โV,T. trf (๐{Cast} V. T)
-| trf_beta : โV,W,T. trf (๐{Appl} V. ๐{Abst} W. T)
+| trf_abst_sn: โV,T. trf V โ trf (โV. T)
+| trf_abst_dx: โV,T. trf T โ trf (โV. T)
+| trf_appl_sn: โV,T. trf V โ trf (โV. T)
+| trf_appl_dx: โV,T. trf T โ trf (โV. T)
+| trf_abbr : โV,T. trf (โV. T)
+| trf_cast : โV,T. trf (โฃV. T)
+| trf_beta : โV,W,T. trf (โV. โW. T)
.
interpretation
(* Basic inversion lemmas ***************************************************)
-fact trf_inv_atom_aux: โI,T. โ[T] โ T = ๐{I} โ False.
+fact trf_inv_atom_aux: โI,T. โ[T] โ T = โช{I} โ False.
#I #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
]
qed.
-lemma trf_inv_atom: โI. โ[๐{I}] โ False.
+lemma trf_inv_atom: โI. โ[โช{I}] โ False.
/2 width=4/ qed-.
-fact trf_inv_abst_aux: โW,U,T. โ[T] โ T = ๐{Abst} W. U โ โ[W] โจ โ[U].
+fact trf_inv_abst_aux: โW,U,T. โ[T] โ T = โW. U โ โ[W] โจ โ[U].
#W #U #T * -T
[ #V #T #HV #H destruct /2 width=1/
| #V #T #HT #H destruct /2 width=1/
]
qed.
-lemma trf_inv_abst: โV,T. โ[๐{Abst}V.T] โ โ[V] โจ โ[T].
+lemma trf_inv_abst: โV,T. โ[โV.T] โ โ[V] โจ โ[T].
/2 width=3/ qed-.
-fact trf_inv_appl_aux: โW,U,T. โ[T] โ T = ๐{Appl} W. U โ
+fact trf_inv_appl_aux: โW,U,T. โ[T] โ T = โW. U โ
โจโจ โ[W] | โ[U] | (๐[U] โ False).
#W #U #T * -T
[ #V #T #_ #H destruct
]
qed.
-lemma trf_inv_appl: โW,U. โ[๐{Appl}W.U] โ โจโจ โ[W] | โ[U] | (๐[U] โ False).
+lemma trf_inv_appl: โW,U. โ[โW.U] โ โจโจ โ[W] | โ[U] | (๐[U] โ False).
/2 width=3/ qed-.
-lemma tif_inv_abbr: โV,T. ๐[๐{Abbr}V.T] โ False.
+lemma tif_inv_abbr: โV,T. ๐[โV.T] โ False.
/2 width=1/ qed-.
-lemma tif_inv_abst: โV,T. ๐[๐{Abst}V.T] โ ๐[V] โง ๐[T].
+lemma tif_inv_abst: โV,T. ๐[โV.T] โ ๐[V] โง ๐[T].
/4 width=1/ qed-.
-lemma tif_inv_appl: โV,T. ๐[๐{Appl}V.T] โ โงโง ๐[V] & ๐[T] & ๐[T].
+lemma tif_inv_appl: โV,T. ๐[โV.T] โ โงโง ๐[V] & ๐[T] & ๐[T].
#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.
+lemma tif_inv_cast: โV,T. ๐[โฃV.T] โ False.
/2 width=1/ qed-.
(* Basic properties *********************************************************)
-lemma tif_atom: โI. ๐[๐{I}].
+lemma tif_atom: โI. ๐[โช{I}].
/2 width=4/ qed.
-lemma tif_abst: โV,T. ๐[V] โ ๐[T] โ ๐[๐ {Abst}V.T].
+lemma tif_abst: โV,T. ๐[V] โ ๐[T] โ ๐[โV.T].
#V #T #HV #HT #H
elim (trf_inv_abst โฆ H) -H /2 width=1/
qed.
-lemma tif_appl: โV,T. ๐[V] โ ๐[T] โ ๐[T] โ ๐[๐{Appl}V.T].
+lemma tif_appl: โV,T. ๐[V] โ ๐[T] โ ๐[T] โ ๐[โV.T].
#V #T #HV #HT #S #H
elim (trf_inv_appl โฆ H) -H /2 width=1/
qed.