Missing Contextual Hypothesis in TCC

[marianomoscato]

Some contextual hypotheses are not included in some TCCs, making them impossible to prove.

See for example the following theory.

missing_hyp: THEORY
BEGIN

  p(b: above(3))(c: nat): bool = 3 <= b + c

  test
  : CONJECTURE
    FORALL(b:nat)
    : b > 3
      IMPLIES FORALL(n: (p(b))): TRUE  

END missing_hyp

The only TCC generated by the type checker is shown below.

% Subtype TCC generated (at line 10, column 27) for  b
    % expected type  above(3)
  % unfinished
test_TCC1: OBLIGATION FORALL (b: nat): b > 3;

Since this TCC is related to the expression p(b) in the lemma test, the antecedent of the implication (b > 3) should be a hypothesis of the TCC as well. Such antecedent is needed to prove the TCC.

[marianomoscato]

This issue is solved (at least) from commit fb640c2670cd34a6b932475c559bee069f4fddd8.