proposition: Lemma composable_facts_rw : forall c u v, composable c u v = composable_facts c u v.
proof: Proof. ir; ap iff_eq; ir. cp H; uh H; ee. cp H; uh H; ee. clear H6. uhg; dj; try am. uhg; ee. am. lu. uhg; ee; lu. rwi H4 H1. uh H1; ee. uhg; ee; try am. uh H7; ee; am. rwi H4 H7. uh H7. ee. am. rwi H4 H7. uh H7. ee. am. uhg; uh H; xd. Qed.
imports: Arith universe