test.zen (1056B)
1 @ being 2 3 ^ attitude precontext 4 fill name wft 5 { vars var 6 fill name a 7 { rest nil } } 8 { pressupositions nil } 9 10 ^ attitude precontext 11 fill name is 12 { vars var 13 fill name a 14 { rest var 15 fill name b 16 { rest nil } } } 17 { pressupositions cons 18 { car term 19 fill head wft 20 { subterms cons 21 { car term 22 fill head b 23 { subterms nil } } 24 { cdr nil } } } 25 { cdr nil } } 26 27 ^ assumption precontext 28 fill name type_is_wft 29 { subcontext being } 30 { judgment term 31 fill head wft 32 { subterms cons 33 { car term 34 fill head a 35 { subterms nil } } 36 { cdr nil } } } 37 { proof done } 38 39 ^ assumption precontext 40 fill name any_type_is_wft 41 { subcontext assumption 42 fill name a_is_type 43 { judgment term 44 fill head is 45 { subterms cons 46 { car term 47 fill head a 48 { subterms nil } } 49 { cdr cons 50 { car term 51 fill head type 52 { subterms nil } } 53 { cdr nil } } } } 54 { precontext being } 55 { subcontext being } 56 { proof done } } 57 { judgment term 58 fill head wft 59 { subterms cons 60 { car term 61 fill head a 62 { subterms nil } } 63 { cdr nil } } } 64 { proof done }