update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / examples / ex_rpx_fwd.ma

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 c4a6b96c4fe38829b77f684ce47346cc358db5f8..efefd445d6b745d923e474d832e232bbf073a592 100644 (file)
--- 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 â\89\9b[T] L2 K i1 i0.
-/3 width=1 by reqx_pair, reqx_sort/ qed.
+      L K s1 s0 â\89\85[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):
-        (â\9dªG,L1 K s1 s0â\9d« â\8a¢ â¬\88 L K s1 s0 â\86\92 L K s1 s0 â\89\9b[T] L2 K i1 i0 → ❪G,L1 K s1 s0❫ ⊢ ⬈[T] L2 K i1 i0) → ⊥.
+        (â\9dªG,L1 K s1 s0â\9d« â\8a¢ â¬\88 L K s1 s0 â\86\92 L K s1 s0 â\89\85[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-.