adt Unit {
  unit()
}

domain Exe67 {
  function F67(x : Int, y : Int) : Int

  function L67() : Int
  function R67() : Int

  axiom LeftUnit67 {
    forall x : Int :: {F67(L67(), x)}
      F67(L67(), x) == L67()
  }

  axiom RightUnit67 {
    forall x : Int :: {F67(x, R67())} 
      F67(x, R67()) == R67()
  }
}

function functionUnit(x : Int) : Unit
    decreases

1. Example of the function:

   function lemmaLEqualR67() : Unit
     ensures L67() == R67()
     decreases
   {let x == (F67(L67(), R67())) in unit()}

2. Example of the function:

   function lemmaLEqualR67() : Unit
     ensures L67() == R67()
     decreases
   {let x == (F67(L67(), R67())) in functionUnit(x)}

In this example, I wanted to prove the postcondition L67() == R67().
Viper will not be able to prove it automatically, therefore I had to provide the body F67(L67(), R67()) with which Viper is able to prove the condition. Silicon is only able to prove the postcondition in Example 2. Somehow in Example 1 Silicon does not use the variable x to help it prove the statement, therefore I created a second example where x is used in the function body using a helper function functionUnit.
This is only an issue for Silicon, Carbon is able to prove the postcondition in both cases.