proposition: Lemma axAA (pS : pSystem) (s t u : pS) : mprv ((s :/\: t) :/\: u <--> s :/\: t :/\: u).
proof: Proof. rule axAI. - do 2 rule axAcase. do 3 Intro. ApplyH axAI. ApplyH axAI. - rule axAcase; Intro. ApplyH axAcase; do 2 Intro. ApplyH axAI. ApplyH axAI. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions