1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LOGIC/datatypes/Sequent".
19 - left hand sides (lhs): A C
20 - right hand sides (rhs): B D
24 include "datatypes/Formula.ma".
26 inductive LHS: Type \def
28 | labst: LHS \to Formula \to LHS
31 inductive RHS: Type \def
33 | rabst: Formula \to RHS \to RHS
36 inductive Sequent: Type \def
37 | pair: LHS \to RHS \to Sequent
40 definition linj: Formula \to LHS \def labst lleaf.
42 definition rinj: Formula \to RHS \def \lambda b. rabst b rleaf.
44 coercion cic:/matita/LOGIC/datatypes/Sequent/linj.con.
46 coercion cic:/matita/LOGIC/datatypes/Sequent/rinj.con.