proposition: Lemma cofmap_secures {X Y : Type} (f : Y -> X) (p : WFT X) (R : X -> X -> Prop) : SecureBy R p -> SecureBy (fun x y => R (f x) (f y)) (cofmap f p).
proof: Proof. induction p in R |- *; simpl; auto. intros. specialize (H (f x) (fun y z : X => R y z \/ R (f x) y)). simpl in H. apply H. apply H0. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)