X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fdefndb.ma;h=745090de4bb719b834c2c96f7424aab879c91d7a;hb=56c4e355b88aa505b64c539053aba92eb86afc2a;hp=4a61bcb2fe7325fdf5546a29abbca669003da228;hpb=9883f04161a9972f0641dd85faf224b4f2846f05;p=helm.git

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma b/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma
index 4a61bcb2f..745090de4 100644
--- 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]]