Reconstruct terms when calling an operation

Currently term arguments are not reconstructed when applying an operation in an environment. This means that any terms which are not dependencies of variables will be missing when presented to the referee.

Example

 ⊢ 1 : ob ;
 A : ob  ⊢ ! A : hom A (1) ;
 A : ob , f : hom A (1) ⊢ !-uniq f : ≡ f (! A) ;

Here the referee will complain that the term representing 1 (called 10) has not been given a value when calling "!".

Solution

To mitigate this, we could store the construction of these arguments in the calling conventions, and make sure to recontruct these objects when calling an operation.