patch for always having Just first in the proof term. Will be useful fot pattern matching at typecheck time !