Open JonasOberhauser opened 2 months ago
Lemma plain_coherence_helper (r s t : relation actid) : r ∩ s⁻¹ ∪ t ≡ ∅₂ -> irreflexive (s ⨾ r). Proof. basic_solver 42.
gives me
All the remaining goals are on the shelf: actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid actid
gives me