levels

server/testgame/TestGame/Levels/Implication/L05_Apply.lean

@@ -24,47 +24,41 @@ $$
 Statement
     "Beweise $A \\Rightarrow F$."
     (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E)
-    (i : D → E) (k : E → F) (m : C → F)
-    (n : G → D) (p : H → E) (q : F → I)
-    (r : H → G) (s : H → I) : A → I := by
+    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
+    (n : H → E) (p : F → I) (q : H → G) (r : H → I) : A → I := by
   intro ha
-  apply q
+  apply p
   apply k
   apply h
   apply f
   assumption
 
 Hint (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E)
-    (i : D → E) (k : E → F) (m : C → F)
-    (n : G → D) (p : H → E) (q : F → I)
-    (r : H → G) (s : H → I) : A → I =>
+    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
+    (n : H → E) (p : F → I) (q : H → G) (r : H → I)  : A → I =>
 "**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
 
 **Robo**: Und dann fängst du am besten wieder mit `intro` an."
 
 HiddenHint (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E)
-    (i : D → E) (k : E → F) (m : C → F)
-    (n : G → D) (p : H → E) (q : F → I)
-    (r : H → G) (s : H → I) (a : A) : I =>
+    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
+    (n : H → E) (p : F → I) (q : H → G) (r : H → I) (a : A) : I =>
 "**Robo**: Na wieder `apply`, was sonst."
 
+-- TODO: Dieser wird falscherweise bei `F` angezeigt
 Hint (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E)
-    (i : D → E) (k : E → F) (m : C → F)
-    (n : G → D) (p : H → E) (q : F → I)
-    (r : H → G) (s : H → I) (a : A) : H =>
+    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
+    (n : H → E) (p : F → I) (q : H → G) (r : H → I) (a : A) : H =>
 "**Robo**: Das sieht nach einer Sackgasse aus…"
 
 Hint (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E)
-    (i : D → E) (k : E → F) (m : C → F)
-    (n : G → D) (p : H → E) (q : F → I)
-    (r : H → G) (s : H → I) (a : A) : C =>
+    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
+    (n : H → E) (p : F → I) (q : H → G) (r : H → I) (a : A) : C =>
 "**Robo**: Nah, da stimmt doch was nicht…"
 
 DisabledTactic tauto
 
+Conclusion
+"Mit einem lauten Ratteln springen die Förderbänder wieder an."
+
 -- https://www.jmilne.org/not/Mamscd.pdf