Finish proof of flipEdge.instIsIrrefl

Pdl/TableauPath.lean

@@ -706,20 +706,30 @@ lemma edge_TransGen_then_mem_History :
 
 lemma PathIn.mem_history_setEqTo_then_lrep {tab : Tableau Hist X} (p : PathIn tab) :
     (∃ Y ∈ (tabAt p).1, Y.setEqTo (nodeAt p)) → (tabAt p).2.2.isLrep := by
-  -- IDEA: should be forbidden by `nrep`?
-  -- (and if we don't have `nrep` then we must have an `lrep` where the tableau ends?)
-  -- Note: first thought we need `Hist = []` as for many things in Soundness.lean, or
-  -- at least that `X` is not in `Hist`, but in fact that should not be needed.
-  sorry
+  rintro ⟨Y, h1, h2⟩
+  generalize h : tabAt p = tp
+  rcases tp with ⟨H, Z, t⟩
+  simp [nodeAt] at h2
+  rw [h] at h2
+  cases t
+  case loc nbas lt nrep next => exact nrep ⟨Y, by aesop⟩
+  case pdl S bas p nrep t    => exact nrep ⟨Y, by aesop⟩
+  case lrep                  => simp [Tableau.isLrep]
+
+lemma single_of_transgen {α} {r} {a c: α} : Relation.TransGen r a c → ∃ b, r a b := by
+  intro h
+  induction h
+  case single b e => use b
+  case tail d e ih => assumption
 
 instance flipEdge.instIsIrrefl : IsIrrefl (PathIn tab) (Relation.TransGen (flip edge)) := by
   constructor
   intro p p_p
   rw [Relation.transGen_swap] at p_p
   have p_in_Hist_p := edge_TransGen_then_mem_History p_p
   have := PathIn.mem_history_setEqTo_then_lrep p ⟨nodeAt p, by simpa⟩
-  -- Now need: lrep has no outgoing edges.
-  sorry
+  rcases (single_of_transgen p_p)
+  with ⟨_, ⟨_, _, _, _, _, _, _, _, h, _⟩ | ⟨_, _, _, _, _, _, _, h, _⟩⟩ <;> rw [h] at this <;> contradiction
 
 /-- The `flip edge` relation in a tableau is well-founded. -/
 theorem flipEdge.wellFounded :