+
+theorem dummy_inv: ∀P,G,M,N. G ⊢ _{P} M: N → ∀A,B.M = D A B →
+ Co P N B ∧ G ⊢_{P} A : B.
+#Pts #G #M #N #t (elim t);
+ [#i #j #Aij #A #b #H destruct
+ |#G1 #P #i #t #_ #A #b #H destruct
+ |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #b #Hl
+ cases (dummy_lift … Hl) #A1 * #b1 * * #eqP #eqA #eqb
+ cases (H1 … eqP) #c1 #t3 <eqb %
+ [@(conv_lift … c1) |<eqA @(weak … t3 t2) ]
+ |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #b #H destruct
+ |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #b #H destruct
+ |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #b #H destruct
+ |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #b #eqA
+ cases (H1 … eqA) #c1 #t3 % // @(trans_conv Pts … c1) @sym_conv //
+ |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct /2/
+ ]
+qed.