pub fn simulation_relation_ty() -> Expr
SimulationRelation: a relation witnessing a simulation (forward simulation). Type: {A C : Type} → (A → C → Prop) → Prop