proposition: Lemma ax_contra s t : mprv ((~~:t ---> ~~: s) ---> (s ---> t)).
proof: Proof. do 2 Intro. ApplyH axDN. Intro. by Apply* 2. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions