More updates to Fsub.

[helm.git] / helm / software / matita / contribs / POPLmark / Fsub / defndb.ma

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma b/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma
index 4a61bcb2fe7325fdf5546a29abbca669003da228..745090de4bb719b834c2c96f7424aab879c91d7a 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma
@@ -18,8 +18,8 @@ include "nat/lt_arith.ma".
 
 (*** representation of Fsub types ***)  
 inductive Typ : Set ≝
-  | TVar : nat → Typ            (* type var *)
-  | Top : Typ                     (* maximum type *)
+  | TVar : nat → Typ          (* type var *)
+  | Top : Typ                 (* maximum type *)
   | Arrow : Typ → Typ → Typ   (* functions *) 
   | Forall : Typ → Typ → Typ. (* universal type *)
 
@@ -224,7 +224,11 @@ definition lifter : nat → nat → nat → nat ≝
 lemma extensional_perm : ∀T.∀f,g.(∀x.f x = g x) → perm T f = perm T g.
 intro;elim T
 [4:whd in ⊢ (??%%);cut (∀x.flift f 1 x = flift g 1 x)
- [autobatch
+ [rewrite > (H f g);
+  [rewrite > (H1 (flift f 1) (flift g 1));
+   [reflexivity
+   |assumption]
+  |assumption]
  |intro;simplify;cases x
   [reflexivity
   |simplify;rewrite > H2;reflexivity]]