* 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) ->
*)
(* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
-
+*)
End HaskProofFlattener.