proposition: Lemma flip_arrow {A : Type} {B : Type} `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature).
proof: Proof. unfold Normalizes in *. unfold relation_equivalence in *. unfold predicate_equivalence in *. simpl in *. unfold respectful. unfold flip in *. intros x x0; split; intros H x1 y H0. - apply NB. apply H. apply NA. apply H0. - apply NB. apply H. apply NA. apply H0. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses