proposition: Lemma ob_facts_rw : forall c x, ob c x = ob_facts c x.
proof: Proof. ir. ap iff_eq; ir. cp H; uh H; ee. cp H; uh H; ee. clear H6. cp H1; uh H1; ee. rwi H H6. uh H6; ee. uhg; xd. uhg; xd. uhg; xd. uhg; xd. rw H8; rw H9; tv. ir. ap H10. lu. am. ir. ap H11; lu. lu. Qed.
imports: Arith universe