Require Import Forms. Inductive NL_arrow : Form -> Form -> Set := | one : forall A, NL_arrow A A | comp : forall A B C, NL_arrow A B -> NL_arrow B C -> NL_arrow A C | beta : forall A B C, NL_arrow (A o B) C -> NL_arrow A (C // B) | beta' : forall A B C , NL_arrow A (C // B) -> NL_arrow (A o B) C | gamma : forall A B C, NL_arrow (A o B) C -> NL_arrow B (A \\ C) | gamma' : forall A B C, NL_arrow B (A \\ C) -> NL_arrow (A o B) C. Hint Resolve one comp beta gamma : ctl. Notation "A -NL-> B" := (NL_arrow A B) (at level 46, right associativity) : lbk_scope. Lemma Dot_mono_left : forall A B C : Form, A -NL-> C -> A o B -NL-> C o B. intros A B C H . apply beta'. eapply comp. (* or apply comp with C *) eexact H. auto with ctl. (* another proof *) Restart. intros; apply beta'; eauto with ctl. Defined. Lemma Dot_mono_right : forall A B C : Form, B -NL-> C -> A o B -NL-> A o C. intros A B C H . apply gamma'. eapply comp. (* or apply comp with C *) eexact H. auto with ctl. Defined. Hint Resolve Dot_mono_left Dot_mono_right :ctl. Lemma Dot_mono : forall A B C D, A -NL-> B -> C -NL-> D -> A o C -NL-> B o D. intros A B C D H H'. eapply comp; eauto with ctl. Defined. Lemma Slash_isotonicity : forall A B C : Form , A -NL-> B -> A // C -NL-> B // C. intros A B C H. apply beta. apply comp with A; auto with ctl. apply beta'. auto with ctl. Defined. Lemma Slash_antitonicity : forall A B C : Form , C -NL-> B -> A // B -NL-> A // C. intros A B C H. apply beta. apply comp with (A // B o B); eauto with ctl. apply beta'; auto with ctl. Defined. Definition Backslash_antitonicity : forall A B C : Form , A -NL-> B -> B \\ C -NL-> A \\ C. intros A B C H. apply gamma. apply comp with (B o B \\ C); eauto with ctl. apply gamma'; auto with ctl. Defined. Definition Backslash_isotonicity : forall A B C : Form, B -NL-> C -> A \\ B -NL-> A \\ C. intros A B C H. apply gamma. apply comp with B;eauto with ctl. apply gamma';auto with ctl. Defined.