has goal Deductions -> is for example has goal ⇐ (has goal is a ->), (is a is inverse of is for example)