liamoc.net
my forest
1\date{2025-11-27T04:46:18Z}
2\taxon{Exercise}
3\author{liamoc}
4\import{shiki-macros}
5\parent{isa-0002}
6\import{dt-macros}
7\put\shiki/language{Isabelle Theory}
8
9\shiki{lemma ‹(∀ x. P x) ⟶ Q ⟹ ∃ x. P x ⟶ Q›}
10
11\solnblock{\shiki{apply (rule ccontr)
12apply (elim impE)
13 apply (intro allI)
14 apply (rule ccontr)
15 apply (erule notE)
16 apply (rule_tac x = x in exI)
17 apply (rule impI)
18 apply (erule notE)
19 apply assumption
20apply (erule notE)
21apply (intro exI)
22apply (rule impI)
23apply assumption
24done}}
25
26