More than 5 years have passed since last update.
SsreflectSample.v
RequireImportssreflectssrbooleqtypessrnat.SectionHilbertSaxiom.VariablesABC:Prop.LemmaHilbertS:(A->B->C)->(A->B)->A->C.Proof.move=>hAiBiChAiBhA.move:hAiBiC.apply.by[].byapply:hAiB.Qed.EndHilbertSaxiom.Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme