X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fdefn.ma;h=95c832efdf4dd6bad0172c23fd3276c101899af1;hb=86e962200667fbd6d77f9680d08f6d5efc59959c;hp=7907405ff9057c62e9644697ee0336eb10cb0764;hpb=a7d6e83ed805988b82f35e8f39934855b156f97a;p=helm.git

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
index 7907405ff..95c832efd 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
@@ -361,6 +361,7 @@ intros.inversion H;intros
   |destruct H5|*:destruct H6]
 qed.
 
+(*
 (* elim vs inversion *)
 lemma JS_trans_TFree: ∀G,T,X.G ⊢ T ⊴ (TFree X) →
   ∀U.G ⊢ (TFree X) ⊴ U → G ⊢ T ⊴ U.
@@ -372,6 +373,7 @@ intros 4.cut (∀Y.TFree Y = TFree X → ∀U.G ⊢ (TFree Y) ⊴ U → G ⊢ T
     |apply (SA_Trans_TVar ? ? ? ? H1);apply (H3 Y);assumption
     |*:destruct H5]]
 qed.
+*)
 
 lemma fv_append : ∀G,H.fv_env (G @ H) = (fv_env G @ fv_env H).
 intro;elim G;simplify;autobatch paramodulation;