fact: Fixpoint pointwise_extension {T : Type} (op : binary_operation T) (l : Tlist) : binary_operation (arrows l T) := match l with | Tnil => fun R R' => op R R' | A :: tl => fun R R' => fun x => pointwise_extension op tl (R x) (R' x) end.
imports: Coq.Classes.Init Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions