X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftif.ma;h=a745dd844cd48247ba4ca5a050b1942999e8b389;hb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;hp=5b89755a7261d49a202f30a598ae2bd93621fdc5;hpb=eb918fc784eacd2094e3986ba321ef47690d9983;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
index 5b89755a7..a745dd844 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
@@ -12,43 +12,43 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/reducibility/trf.ma".
+include "basic_2/reducibility/trf.ma".
 
 (* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
 
-definition tif: predicate term ≝ λT. 𝐑[T] → False.
+definition tif: predicate term ≝ λT. 𝐑⦃T⦄ → ⊥.
 
 interpretation "context-free irreducibility (term)"
    'NotReducible T = (tif T).
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → False.
+lemma tif_inv_abbr: ∀V,T. 𝐈⦃ⓓV.T⦄ → ⊥.
 /2 width=1/ qed-.
 
-lemma tif_inv_abst: ∀V,T. 𝐈[ⓛV.T] → 𝐈[V] ∧ 𝐈[T].
+lemma tif_inv_abst: ∀V,T. 𝐈⦃ⓛV.T⦄ → 𝐈⦃V⦄ ∧ 𝐈⦃T⦄.
 /4 width=1/ qed-.
 
-lemma tif_inv_appl: ∀V,T. 𝐈[ⓐ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. 𝐈[ⓣV.T] → False.
+lemma tif_inv_cast: ∀V,T. 𝐈⦃ⓣV.T⦄ → ⊥.
 /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] →  𝐈[ⓛ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] → 𝐈[ⓐ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.