proposition: Lemma flip_arrow `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signatureT).
proof: Proof. unfold Normalizes in *. intros. rewrite NA, NB. firstorder. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses