proposition: Lemma le'_irrel n m (p q : le' n m) : p = q.
proof: Proof. revert q. induction p using le'_dep. intros q. depelim q. reflexivity. exfalso. now eapply le'prf_nocycle in q. intros q. depelim q. exfalso. clear IHp. now eapply le'prf_nocycle in p. f_equal. apply IHp. Defined.
imports: Equations(Equations)