fill in lots of missing proofs

[coq-hetmet.git] / src / HaskProofFlattener.v

diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v
index 82bc678..fcc2a37 100644 (file)
--- a/src/HaskProofFlattener.v
+++ b/src/HaskProofFlattener.v
@@ -133,6 +133,7 @@ Section HaskProofFlattener.
    * it might help to have the definition for "Inductive ND" (see
    * NaturalDeduction.v) handy as a cross-reference.
    *)
    * it might help to have the definition for "Inductive ND" (see
    * NaturalDeduction.v) handy as a cross-reference.
    *)

+(*

   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
     : forall h c,
       (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->
   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
     : forall h c,
       (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->

@@ -392,6 +393,6 @@ Section HaskProofFlattener.
       *)
 
   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
       *)
 
   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)

-
+*)

 End HaskProofFlattener.
 
 End HaskProofFlattener.