proposition: Theorem cast_spec : forall A dom₁ dom₂ (Heq : Dom.eq dom₁ dom₂) (m : t A dom₁), eq (cast Heq m) m.
proof: Proof. repeat intro. apply cast_spec_find. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface