X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofStratified.v;h=177bd6d3911e9bacc798cf47077a93d71976fef1;hp=ee475da8a612863537664b1526b1d271af5e20e5;hb=d6342fb07462cc126df948459ce98ea9caadb95c;hpb=e539b49ae3148ab1967b5ea0709734171180b86d

diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v
index ee475da..177bd6d 100644
--- a/src/HaskProofStratified.v
+++ b/src/HaskProofStratified.v
@@ -231,7 +231,7 @@ Section HaskProofStratified.
       Alternating c'.
 
   Require Import Coq.Logic.Eqdep.
-
+(*
   Lemma magic a b c d ec e :
     ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
     ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
@@ -318,7 +318,7 @@ Section HaskProofStratified.
       destruct c; try destruct o; inversion H.
       destruct j.
       Admitted.
-
+*)
   (* any proof in organized form can be "dis-organized" *)
   (*
   Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.