leanExample context := 2