  This is a basic property of justifications assumed in combinatory  logic and \(\lambda\)  -calculi (Troelstra and Schwichtenberg  1996), Brouwer-Heyting-Kolmogorov semantics (Troelstra and van Dalen  1988), Kleene realizability (Kleene 1945), the Logic of Proofs  \(\mathsf{LP}\),  etc.