F. Stuart, R. L. Allen, D. J. Constable, W. Howe, and . Aitken, The semantics of reflected proof, Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp.95-197, 1990.

T. Altenkirch, C. Mcbride, and W. Swierstra, Observational equality, now!, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.57-68, 2007.
DOI : 10.1145/1292597.1292608

H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, 1992.

H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics. Sole Distributors for the, 1984.

E. Barzilay, Implementing Reflection in Nuprl, 2006.

R. L. Constable, Using Reflection to Explain and Enhance Type Theory, Proof and Computation, pp.65-100, 1994.
DOI : 10.1007/978-3-642-79361-5_3

T. Coquand and C. Paulin, Inductively defined types, COLOG-88, pp.50-66, 1990.
DOI : 10.1007/3-540-52335-9_47

M. Felleisen, On the expressive power of programming languages, Science of Computer Programming, pp.134-151, 1990.

J. Girard, P. Taylor, and Y. Lafont, Proofs and types, 1989.

B. Nordström, K. Petersson, and J. M. Smith, Programming in Martin- Löf 's Type Theory: An Introduction, 1990.

F. Pfenning and C. Paulin-mohring, Inductively defined types in the Calculus of Constructions, Proceedings of the 5th International Conference on Mathematical Foundations of Programming Semantics, pp.209-228, 1990.
DOI : 10.1007/BFb0040259

C. Benjamin and . Pierce, Types and programming languages, 2002.

J. Rehof, Strong normalization for non-structural subtyping via saturated sets, Information Processing Letters, vol.58, issue.4, pp.157-162, 1996.
DOI : 10.1016/0020-0190(96)00056-7

K. Scharp, Truth and internalizability. Draft available from http://people. cohums.ohio-state, p.1, 2010.

V. Sjöberg and A. Stump, Equality, Quasi-Implicit Products, and Large Eliminations, Workshop on Intersection Types and Related Systems (ITRS), 2010.
DOI : 10.4204/EPTCS.45.7

T. Streicher, Investigations into Intensional Type Theory, 1993.

J. A. Vaughan, Aura: Programming with Authorization and Audit, 2009.

?. Assume-t, Take arbitrary u ? [[S 1 ]] ? . By definition, we know (t u) ? [, With our reduction strategy, (t u) ? (t ? u). By IH(CR 2)

?. Assume-t-is, By definition, we know (t ? u) ? [ With our reduction strategy By IH(CR 1), u is closed, thus we know (t u) is closed, By IH(CR, vol.3, issue.1

?. Assume-t, We know that ? is non-empty (for example, V ? ?) Take an arbitrary reducibility candidate R. By definition of, By IH(CR 1), t ? V

?. Assume-t, Consider arbitrary reducibility candidate R. By definition, t ?, By IH, issue.2

?. Assume-t-is, Take arbitrary reducibility candidate R. By definition, t ? ? We know that t ? t ? and t is closed