- contexts: P Q
*)
+include "datatypes/Proof.ma".
include "datatypes/Sequent.ma".
inductive Context: Type \def
| leaf: Context
- | abst: Context \to Sequent \to Context
+ | abst: Context \to Proof \to Proof \to Sequent \to Context
.
-
+(*
definition inj: Sequent \to Context \def abst leaf.
coercion cic:/matita/LOGIC/datatypes/Context/inj.con.
+*)