proposition: Lemma predicate_implication_pointwise (l : Tlist) : Proper (@predicate_implication l ==> pointwise_lifting impl l) id.
proof: Proof. do 2 red. unfold predicate_implication. auto. Qed.
imports: Relation_Definitions Coq.Classes.Morphisms Coq.Program.Program