- Context Γ (Δ:CoercionEnv Γ).
-
- (* An organized deduction has been reorganized into contiguous blocks whose
- * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth. The boolean
- * indicates if non-PCF rules have been used *)
- Inductive OrgR : Tree ??(@FCJudg Γ) -> Tree ??(@FCJudg Γ) -> Type :=