proposition: Lemma flip_flip : forall a, flip (flip a) = a.
proof: Proof. ir. apply by_cases with (like a); ir. rw flip_like. rw target_flip. rw source_flip. rw arrow_flip. uh H. sy; am. am. am. wr like_flip. am. rw flip_not_like. rw flip_not_like. tv. am. uhg; ir. ap H. rw like_flip. am. Qed.
imports: Arith functions