Add LoadPath "../Light". Require Import Forms. Require Import Hilbert. Require Import Semantics. Require Import Sequents. Require Import List. Require Import ZArith. Open Scope Z_scope. Open Scope lbk_scope. Ltac beta := apply beta. Ltac gamma := apply gamma. Ltac beta' := apply beta'. Ltac gamma' := apply gamma'. Ltac comp X := apply comp with (B:=X). Ltac ecomp := eapply comp. Ltac one := apply one. Definition deriv1 : s -NL-> (s o np) // np. Admitted. Definition deriv2 : (s//np) o np -NL-> s. Admitted. Definition deriv3 : np o (np \\ (s // np)) o np -NL-> s. Admitted. Definition deriv4 : (np//n)o(n//n o n) -NL-> np. Admitted. Definition Dot_mono_right : forall A B C : Form, B -NL-> C -> A o B -NL-> A o C. Admitted. Definition Dot_mono : forall A B C D, A -NL-> B -> C -NL-> D -> A o C -NL-> B o D. Admitted. Definition isotonicity : forall A B C : Form , A -NL-> B -> A // C -NL-> B // C. Admitted. Definition antitonicity: forall A B C : Form , C -NL-> B -> A // B -NL-> A // C. Admitted. Definition antitonicity': forall A B C : Form , A -NL-> B -> B \\ C -NL-> A \\ C. Admitted. Definition isotonicity' : forall A B C : Form, B -NL-> C -> A \\ B -NL-> A \\ C. Admitted. Definition lifting: forall A B, A -NL-> B//(A\\B). Admitted. Definition lifting': forall A B, A -NL-> (B//A)\\B. Admitted. Lemma ex3' : np o (np \\ (s // np)) o np -NL-> s. Admitted.