proposition: Lemma paco2_eqit_refl : forall E R r (t : itree E R), paco2 (eqit_ eq true true id) r t t.
proof: Proof. intros. eapply paco2_mon with (r := bot2). { enough (t ≈ t); auto. reflexivity. } { contradiction. } Qed.
imports: Paco(paco) ITree(Core.ITreeDefinition Eq.Eqit)