proposition: Theorem gen_hsound C : gen C -> prv ([af C] ---> Bot).
proof: Proof. elim => {C} [C|p C|s t C _ IHs _ IHt|s t C _ IH|s C _ IH] /=. - rewrite -> andU,afp1. exact: axAEl. - rewrite -> andU,andU,afp1,afn1. rule axAcase. Intro. ApplyH axAcase. do 2 Intro. Apply* 1. - rewrite -> andU,afp1. rewrite -> andU,<- af1n in IHs. rewrite -> andU,<- af1p in IHt. rule axAcase. do 2 Intro. ApplyH IHs. ApplyH axAI. Intro. ApplyH IHt. ApplyH axAI. Apply* 2. - rewrite -> andU,afn1,dmI,axAA. by rewrite -> andU,->andU, <- af1n, <-af1p in IH. - rewrite <- axDF, -> andU, -> (afn1 (fAX s)). rewrite <- (modular_hilbert.axDN s), -> box_request. rewrite -> andU,<- af1n in IH. rewrite <- IH. rule axAcase. exact: axDBD. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)