parameters: (self,decls,proof)
docstring: Apply a proof to a list of goals, producing subgoals, or None if
          the proof fails.
docstring_summary: Apply a proof to a list of goals, producing subgoals, or None if
          the proof fails.
docstring_tokens: Apply a proof to a list of goals producing subgoals or None if the proof fails .
function: def apply_proof(self,decls,proof):
          """ Apply a proof to a list of goals, producing subgoals, or None if
          the proof fails. """
  
          with ia.ASTContext(proof):
              if len(decls) == 0:
                  return []
              if isinstance(proof,ia.SchemaInstantiation):
                  m = self.match_schema(decls[0],proof)
                  return None if m is None else m + decls[1:]
              elif isinstance(proof,ia.LetTactic):
                  return self.let_tactic(decls,proof)
              elif isinstance(proof,ia.ComposeTactics):
                  return self.compose_proofs(decls,proof.args)
              elif isinstance(proof,ia.AssumeTactic):
                  return self.assume_tactic(decls,proof)
              elif isinstance(proof,ia.UnfoldTactic):
                  return self.unfold_tactic(decls,proof)
              elif isinstance(proof,ia.ForgetTactic):
                  return self.forget_tactic(decls,proof)
              elif isinstance(proof,ia.ShowGoalsTactic):
                  return self.show_goals_tactic(decls,proof)
              elif isinstance(proof,ia.DeferGoalTactic):
                  return self.defer_goal_tactic(decls,proof)
              elif isinstance(proof,ia.DeferGoalTactic):
                  return self.defer_goal_tactic(decls,proof)
              elif isinstance(proof,ia.LetTactic):
                  return self.let_tactic(decls,proof)
              elif isinstance(proof,ia.IfTactic):
                  return self.if_tactic(decls,proof)
              elif isinstance(proof,ia.NullTactic):
                  return decls
              elif isinstance(proof,ia.PropertyTactic):
                  return self.property_tactic(decls,proof)
              elif isinstance(proof,ia.FunctionTactic):
                  return self.function_tactic(decls,proof)
              elif isinstance(proof,ia.TacticTactic):
                  return self.tactic_tactic(decls,proof)
              elif isinstance(proof,ia.ProofTactic):
                  return self.proof_tactic(decls,proof)
              elif isinstance(proof,ia.WitnessTactic):
                  return self.witness_tactic(decls,proof)
              assert False,"unknown proof type {}".format(type(proof))
function_tokens: def apply_proof ( self , decls , proof ) : with ia . ASTContext ( proof ) : if len ( decls ) == 0 : return [ ] if isinstance ( proof , ia . SchemaInstantiation ) : m = self . match_schema ( decls [ 0 ] , proof ) return None if m is None else m + decls [ 1 : ] elif isinstance ( proof , ia . LetTactic ) : return self . let_tactic ( decls , proof ) elif isinstance ( proof , ia . ComposeTactics ) : return self . compose_proofs ( decls , proof . args ) elif isinstance ( proof , ia . AssumeTactic ) : return self . assume_tactic ( decls , proof ) elif isinstance ( proof , ia . UnfoldTactic ) : return self . unfold_tactic ( decls , proof ) elif isinstance ( proof , ia . ForgetTactic ) : return self . forget_tactic ( decls , proof ) elif isinstance ( proof , ia . ShowGoalsTactic ) : return self . show_goals_tactic ( decls , proof ) elif isinstance ( proof , ia . DeferGoalTactic ) : return self . defer_goal_tactic ( decls , proof ) elif isinstance ( proof , ia . DeferGoalTactic ) : return self . defer_goal_tactic ( decls , proof ) elif isinstance ( proof , ia . LetTactic ) : return self . let_tactic ( decls , proof ) elif isinstance ( proof , ia . IfTactic ) : return self . if_tactic ( decls , proof ) elif isinstance ( proof , ia . NullTactic ) : return decls elif isinstance ( proof , ia . PropertyTactic ) : return self . property_tactic ( decls , proof ) elif isinstance ( proof , ia . FunctionTactic ) : return self . function_tactic ( decls , proof ) elif isinstance ( proof , ia . TacticTactic ) : return self . tactic_tactic ( decls , proof ) elif isinstance ( proof , ia . ProofTactic ) : return self . proof_tactic ( decls , proof ) elif isinstance ( proof , ia . WitnessTactic ) : return self . witness_tactic ( decls , proof ) assert False , "unknown proof type {}" . format ( type ( proof ) )