proposition: Lemma morph_id {A OA} (tA : t A OA) : morph OA OA (fun x => x).
proof: Proof. constructor; intros. - apply PO.morph_id. - apply PO.eq_refl. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat