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