- we polarized binders to control zeta reduction

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / trf.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
index 83306d2de3656fbe3b36b89160a5b9960cabc71a..6d6993de3f137b561d551be5533c83d182ead802 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
@@ -23,7 +23,7 @@ inductive trf: predicate term ≝
 | 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   : â\88\80V,T.           trf (â\93£V. T)
+| trf_cast   : â\88\80V,T.           trf (â\93\9dV. T)
 | trf_beta   : ∀V,W,T. trf (ⓐV. ⓛW. T)
 .
 
@@ -33,7 +33,7 @@ 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} → ⊥.
 #I #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
@@ -45,10 +45,10 @@ fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T =  ⓪{I} → False.
 ]
 qed.
 
-lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → False.
+lemma trf_inv_atom: ∀I. 𝐑⦃⓪{I}⦄ → ⊥.
 /2 width=4/ qed-.
 
-fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T =  ⓛ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/
@@ -60,11 +60,11 @@ fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T =  ⓛW. U → 𝐑[W] ∨ 𝐑[U
 ]
 qed.
 
-lemma trf_inv_abst: ∀V,T. 𝐑[ⓛ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 =  ⓐW. U →
-                       ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+fact trf_inv_appl_aux: ∀W,U,T. 𝐑⦃T⦄ → T =  ⓐW. U →
+                       ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
 #W #U #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
@@ -77,5 +77,5 @@ fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T =  ⓐW. U →
 ]
 qed.
 
-lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+lemma trf_inv_appl: ∀W,U. 𝐑⦃ⓐW.U⦄ → ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
 /2 width=3/ qed-.