my forest
better proof
+6
-12
+6
-12
trees/isa/isa-000Y.tree
+6
-12
trees/isa/isa-000Y.tree
···
9
9
\shiki{lemma ‹⟦∀ x. ¬ R x ⟶ R (M x); ∃ x. R x ⟧ ⟹ ∃ x. R x ∧ R (M (M x))›}
10
10
11
11
\solnblock{\shiki{apply (erule exE)
12
-
apply (frule_tac x = a in allE, assumption)
13
-
apply (drule_tac x = a in spec)
12
+
apply (rename_tac a)
13
+
apply (frule_tac x = a in spec)
14
14
apply (frule_tac x = "M a" in spec)
15
15
apply (drule_tac x = "M (M a)" in spec)
16
-
apply (drule disjCI)+
17
-
apply (elim disjE)
18
-
apply (rule_tac x = a in exI; intro conjI; assumption)
19
-
apply (rule_tac x = "M a" in exI; intro conjI; assumption)
20
-
apply (rule_tac x = a in exI; intro conjI; assumption)
21
-
apply (rule_tac x = a in exI; intro conjI; assumption)
22
-
apply (rule_tac x = a in exI; intro conjI; assumption)
23
-
apply (rule_tac x = "M a" in exI; intro conjI; assumption)
24
-
apply (rule_tac x = a in exI; intro conjI; assumption)
25
-
apply (rule_tac x = a in exI; intro conjI; assumption)
16
+
apply (drule disjCI)
17
+
apply (drule disjCI)
18
+
apply (drule disjCI)
19
+
apply (elim disjE;rule exI; rule conjI; assumption)
26
20
done}}
27
21
28
22