all_goals
  apply Relation.ReflTransGen.mono
  intro w v
  rw [IHα w v]
  tauto
case mp
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate M (subst_in_P σ α)) w v → Relation.ReflTransGen (relate (subst_in_model σ M) α) w v

case mpr
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate (subst_in_model σ M) α) w v → Relation.ReflTransGen (relate M (subst_in_P σ α)) w v
no goals