pub fn backward_simulation_ty() -> Expr
BackwardSimulation: a relation witnessing backward simulation. Type: {A C : Type} → (C → A → Prop) → Prop