kdrag.tele.axiom_sig

kdrag.tele.axiom_sig(f: FuncDeclRef, tele0: Telescope, T: SubSort) → Proof

Assign signature to a function f with a telescope of arguments tele0 as an axiom

Parameters:

• f (FuncDeclRef)

• tele0 (Telescope)

• T (SubSort)

Return type:

Proof