proposition: Lemma axADr (pS : pSystem) (s t u : pS) : mprv ((s :\/: t) :/\: u <--> s :/\: u :\/: t :/\: u).
proof: Proof. rule axAI. - rule axAcase. rule axOE. rewrite <- axOIl. exact: axAI. rewrite <- axOIr. exact: axAI. - rule axOE; rule axAcase. rewrite <- axOIl. exact: axAI. rewrite <- axOIr. exact: axAI. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions