proposition: Lemma o'o_pred: forall n (a: test), o' (o_pred n a) ≡ g_prd _ _ a with o'o_npred: forall n (a: test), o' (o_npred n a) ≡ g_prd _ _ (!a).
proof: Proof. destruct a. symmetry. apply inj_bot. symmetry. apply inj_top. setoid_rewrite inj_cup. apply cup_weq; apply o'o_pred. setoid_rewrite inj_cap. apply dot_weq; apply o'o_pred. apply o'o_npred. reflexivity. destruct a. symmetry. etransitivity. apply inj_weq. apply negbot. apply inj_top. symmetry. etransitivity. apply inj_weq. apply negtop. apply inj_bot. etransitivity. 2: apply inj_weq; symmetry; apply negcup. rewrite inj_cap. apply dot_weq; apply o'o_npred. etransitivity. 2: apply inj_weq; symmetry; apply negcap. rewrite inj_cup. apply cup_weq; apply o'o_npred. etransitivity. 2: apply inj_weq; symmetry; apply negneg. apply o'o_pred. reflexivity. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms