X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fexamples%2Fex_rpx_fwd.ma;h=efefd445d6b745d923e474d832e232bbf073a592;hp=c4a6b96c4fe38829b77f684ce47346cc358db5f8;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hpb=613d8642b1154dde0c026cbdcd96568910198251

diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_rpx_fwd.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_rpx_fwd.ma
index c4a6b96c4..efefd445d 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_rpx_fwd.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_rpx_fwd.ma
@@ -12,7 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/static/reqx_fqup.ma".
+include "static_2/static/reqg_fqup.ma".
+include "static_2/static/reqx.ma".
 include "basic_2/rt_transition/lpx.ma".
 include "basic_2/rt_transition/rpx.ma".
 
@@ -35,8 +36,8 @@ lemma ex_rpx_fwd_1 (G) (K) (s1) (s0):
 /3 width=1 by lpx_pair, lpx_bind_refl_dx, cpx_eps/ qed.
 
 lemma ex_rpx_fwd_2 (K) (s1) (s0) (i1) (i0):
-      L K s1 s0 ≛[T] L2 K i1 i0.
-/3 width=1 by reqx_pair, reqx_sort/ qed.
+      L K s1 s0 ≅[T] L2 K i1 i0.
+/4 width=1 by reqg_refl, reqg_pair, reqg_sort, teqg_sort/ qed.
 
 lemma ex_rpx_fwd_3 (G) (K) (s1) (s0) (i1) (i0):
       ❪G,L1 K s1 s0❫ ⊢ ⬈[T] L2 K i1 i0 → ⊥.
@@ -50,5 +51,5 @@ qed-.
 (* Main properties **********************************************************)
 
 theorem ex_rpx_fwd (G) (K) (s1) (s0) (i1) (i0):
-        (❪G,L1 K s1 s0❫ ⊢ ⬈ L K s1 s0 → L K s1 s0 ≛[T] L2 K i1 i0 → ❪G,L1 K s1 s0❫ ⊢ ⬈[T] L2 K i1 i0) → ⊥.
+        (❪G,L1 K s1 s0❫ ⊢ ⬈ L K s1 s0 → L K s1 s0 ≅[T] L2 K i1 i0 → ❪G,L1 K s1 s0❫ ⊢ ⬈[T] L2 K i1 i0) → ⊥.
 /3 width=7 by ex_rpx_fwd_3, ex_rpx_fwd_2, ex_rpx_fwd_1/ qed-.