Hello,

I am trying to solve this exercise

Exercise: 1 star, standard (subtype_instances_tf_2)

from this chapter

https://softwarefoundations.cis.upenn.edu/plf-current/Sub.html

This statemen below. Is it true?

```
∃S,
S <: S→S
```

This is what I think about it:

Going to use 2 rules:

S_Refl and S_Arrow

exists S,

S <: S->S ??? is it true or false, let’s try Exists (S->S)

then

S -> S <: (S -> S) -> (S -> S)

S1 S2 T1 T2 According to S_Arrow we should have 2 statements

Statement 1. (S -> S) <: S

AND

Statement 2. S <: (S -> S)

but it is a contradiction. So answer is False? Is it correct? is it a contradiction?

Thanks,

Nat