proposition: Lemma cofmap_secures: forall (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. intros X Y f p. induction p. intros. simpl. intros. simpl in H. apply H. intros. simpl in H. simpl in H0. simpl. intros. remember (H (f x) (fun y z => R y z \/ R (f x) y)). simpl in s. apply s. apply H0. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)